00100	(LE(ADD1(J) X1) ∧ LE(X1 SUB1(CN))) → LE(A(X1) A(ADD1(X1)));
00200	(LE(U X1) ∧ LE( X1 SUB1(I)) ∧ LE(SUB1(I) CN))→ LE(A(X1) BIG);
00300	(LE(U X1) ∧ LE(X1 J) ∧ LE(J SUB1 (CN))) → LE(A(X1) A(ADD1(J)));
00400	E(BIG A(LOC));
00500	LE(U LOC) ∧ LE(LOC J) ;
00600	LE(ADD1 (U) I);
00700	E(LOC J);
00800	LE(ADD1(J) I);
00900	LE(ADD1 (U) J) ∧ LE(J CN);
01100	
     

00100	((((LE(X2 X1) ∧ LE(X1 X3)) → LE(A(X1) A(X4))) ∧ LE(X5 X3)) →((LE(X2 X6) ∧ LE(X6 X5))→LE(A(X6) A(X4)))) ;
00200	;
     

00100	L(X1 X2)→LE(X1 X2);
00200	LE(X1 X2)→LE(SUB1(X1) SUB1(X2));
00300	LE(SUB1(X1) X1);
00400	(LE(X1 X2) ∧LE(X2 X3))→LE(X1 X3);
00500	E(SUB1(ADD1(X1)) X1);
00600	E(ADD1(SUB1(X1)) X1);
00700	;
     

00100	∀(X1)((LE(U X1) ∧ LE(X1 SUB1(J)) ∧ LE(SUB1(J) SUB1(CN))) → LE(A(X1) A(J)));
00200	;